| Definitions | Realizer, t  T, False, Id,  x:A. B(x), IdLnk, Knd, Type, R-da(R;i), rcv(l,tg), Void, f(x)?z,  , Top, x:A  B(x), x:A B(x), P & Q, P   Q, P  Q, @loc: only members of L read x, P Q, f || g, es realizer ind Rrframe compseq tag def,  b, Rplus-right(x1), Rplus-left(x1), Rplus?(x1), @loc: k sends only on links in L, es realizer ind Rbframe compseq tag def, @loc: k writes only members of L, es realizer ind Raframe compseq tag def, @loc precondition for a(v:T):P State(ds) v, es realizer ind Rpre compseq tag def, sends knd(v:T) on l:tagged(g,State(ds),v):dt, es realizer ind Rsends compseq tag def, @loc effect knd(v:T) x := f State(ds) v , es realizer ind Reffect compseq tag def, only events in L send on lnk with tag, es realizer ind Rsframe compseq tag def, @loc only events in L change x:T, es realizer ind Rframe compseq tag def, @loc x initially v:T, es realizer ind Rinit compseq tag def, KindDeq, destination(l),  x.A(x),  x. t(x), source(l), f  g, es realizer ind Rplus compseq tag def, True, Prop, left right, , es realizer ind Rnone compseq tag def, left+right, s = t, Unit, type List, State(ds), a:A fp B(a), DeclaredType(ds;x), rec(x.A(x)), R-interface(A;B), f(x),  x:A. B(x), {x:A| B(x) }, Atom$n,  A, if b t else f fi, b,  , x dom(f), true, <a,b>,  T, f(a) |